reasoning mcginness
Automated Theorem Provers Help Improve Large Language Model Reasoning
McGinness, Lachlan, Baumgartner, Peter
The release of models like GPT [3] and Gemini [28] through platforms like ChatGPT and Bard have transformed Large Language Models (LLMs) into general-purpose tools that can be used by everyone. Although designed for next token prediction, LLMs have been shown to have emergent abilities and are able to perform a wide variety of tasks without task-specific training data [3, 20, 25, 30, 31]. Unfortunately, LLMs also frequently return wrong results, such as fictitious claims ("hallucinations") or conclusions that defy common sense or (naive qualitative) physics [13, 16, 27]. Such shortcoming may or may not be obvious but in any case impact trustworthiness. A recent famous example was a lawyer who submitted a legal brief generated by ChatGPT which contained many errors and false references [5, 6]. Asking the LLM for an explanation might help, but the explanation might contain errors again and does not necessarily reflect the process used to obtain its answer. Equipping and checking LLMs with trustworthy (logical) reasoning remains to be a current major problem [21, 22]. A general approach to address this problem equips LLMs with external functionality [8, 10, 13, 19, 21]. These equipped models are referred to as Augmented Language Models (ALMs).